<html>
<head><meta charset="utf-8"><title>RustHorn · wg-formal-methods · Zulip Chat Archive</title></head>
<h2>Stream: <a href="https://rust-lang.github.io/zulip_archive/stream/183875-wg-formal-methods/index.html">wg-formal-methods</a></h2>
<h3>Topic: <a href="https://rust-lang.github.io/zulip_archive/stream/183875-wg-formal-methods/topic/RustHorn.html">RustHorn</a></h3>

<hr>

<base href="https://rust-lang.zulipchat.com">

<head><link href="https://rust-lang.github.io/zulip_archive/style.css" rel="stylesheet"></head>

<a name="201423853"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/183875-wg-formal-methods/topic/RustHorn/near/201423853" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> Shnatsel <a href="https://rust-lang.github.io/zulip_archive/stream/183875-wg-formal-methods/topic/RustHorn.html#201423853">(Jun 19 2020 at 18:11)</a>:</h4>
<p>Paper on CHC-based automatic property verification leveraging Rust's ownership, reminiscent of prusti: <a href="https://arxiv.org/abs/2002.09002">https://arxiv.org/abs/2002.09002</a></p>



<a name="201424015"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/183875-wg-formal-methods/topic/RustHorn/near/201424015" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> Shnatsel <a href="https://rust-lang.github.io/zulip_archive/stream/183875-wg-formal-methods/topic/RustHorn.html#201424015">(Jun 19 2020 at 18:13)</a>:</h4>
<p>I'm not sure if any of the authors are here, but you can talk to them at <a href="https://www.reddit.com/r/rust/comments/hbejpj/">https://www.reddit.com/r/rust/comments/hbejpj/</a></p>



<a name="201552418"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/183875-wg-formal-methods/topic/RustHorn/near/201552418" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> Xavier Denis <a href="https://rust-lang.github.io/zulip_archive/stream/183875-wg-formal-methods/topic/RustHorn.html#201552418">(Jun 21 2020 at 20:57)</a>:</h4>
<p>My thesis is based on a similar approach though I'm not targeting CHCs and I'm putting a particular effort in keeping the source language approachable for non CS people.</p>



<a name="201552462"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/183875-wg-formal-methods/topic/RustHorn/near/201552462" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> Xavier Denis <a href="https://rust-lang.github.io/zulip_archive/stream/183875-wg-formal-methods/topic/RustHorn.html#201552462">(Jun 21 2020 at 20:58)</a>:</h4>
<p>I've read the RustHorn paper quite a few times though. The approach of representing borrows as a pair of values is key imo</p>



<a name="201553502"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/183875-wg-formal-methods/topic/RustHorn/near/201553502" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> DPC <a href="https://rust-lang.github.io/zulip_archive/stream/183875-wg-formal-methods/topic/RustHorn.html#201553502">(Jun 21 2020 at 21:26)</a>:</h4>
<p>would love to read it some day once it's published <span aria-label="slight smile" class="emoji emoji-1f642" role="img" title="slight smile">:slight_smile:</span></p>



<a name="201554275"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/183875-wg-formal-methods/topic/RustHorn/near/201554275" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> Xavier Denis <a href="https://rust-lang.github.io/zulip_archive/stream/183875-wg-formal-methods/topic/RustHorn.html#201554275">(Jun 21 2020 at 21:46)</a>:</h4>
<p>I'll have a 20 page summary of this summer's work in ~1 month :)</p>



<a name="201554286"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/183875-wg-formal-methods/topic/RustHorn/near/201554286" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> Xavier Denis <a href="https://rust-lang.github.io/zulip_archive/stream/183875-wg-formal-methods/topic/RustHorn.html#201554286">(Jun 21 2020 at 21:47)</a>:</h4>
<p>It describes a deductive verification system for a small subset of mir (only box + refs + pairs / sums) but includes a proof of correctness and all the fun stuff :)</p>



<a name="201554448"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/183875-wg-formal-methods/topic/RustHorn/near/201554448" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> DPC <a href="https://rust-lang.github.io/zulip_archive/stream/183875-wg-formal-methods/topic/RustHorn.html#201554448">(Jun 21 2020 at 21:52)</a>:</h4>
<p>nice <span aria-label="slight smile" class="emoji emoji-1f642" role="img" title="slight smile">:slight_smile:</span></p>



<a name="201556561"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/183875-wg-formal-methods/topic/RustHorn/near/201556561" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> RalfJ <a href="https://rust-lang.github.io/zulip_archive/stream/183875-wg-formal-methods/topic/RustHorn.html#201556561">(Jun 21 2020 at 22:54)</a>:</h4>
<p><span class="user-mention silent" data-user-id="312719">Xavier Denis</span> <a href="#narrow/stream/183875-wg-formal-methods/topic/RustHorn/near/201552462">said</a>:</p>
<blockquote>
<p>I've read the RustHorn paper quite a few times though. The approach of representing borrows as a pair of values is key imo</p>
</blockquote>
<p>their use of prophecy variables in ingenious. it's a formal take on borrowing that's entirely different from my lifetime logic. i still have to fully understand what it means.</p>



<a name="201588556"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/183875-wg-formal-methods/topic/RustHorn/near/201588556" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> Xavier Denis <a href="https://rust-lang.github.io/zulip_archive/stream/183875-wg-formal-methods/topic/RustHorn.html#201588556">(Jun 22 2020 at 10:13)</a>:</h4>
<p>it also leads to a super natural encoding for deductive verification, since prophecy variables are represented by non-determinism.</p>



<a name="201588643"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/183875-wg-formal-methods/topic/RustHorn/near/201588643" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> Xavier Denis <a href="https://rust-lang.github.io/zulip_archive/stream/183875-wg-formal-methods/topic/RustHorn.html#201588643">(Jun 22 2020 at 10:14)</a>:</h4>
<p>smt solvers love all the constraints that emerge</p>



<a name="201684047"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/183875-wg-formal-methods/topic/RustHorn/near/201684047" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> Yusuke Matsushita <a href="https://rust-lang.github.io/zulip_archive/stream/183875-wg-formal-methods/topic/RustHorn.html#201684047">(Jun 23 2020 at 03:11)</a>:</h4>
<p>Thank you for sharing the paper here! I'm the first author of the paper. Ask me anything <span aria-label="+1" class="emoji emoji-1f44d" role="img" title="+1">:+1:</span></p>



<a name="201684327"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/183875-wg-formal-methods/topic/RustHorn/near/201684327" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> Yusuke Matsushita <a href="https://rust-lang.github.io/zulip_archive/stream/183875-wg-formal-methods/topic/RustHorn.html#201684327">(Jun 23 2020 at 03:19)</a>:</h4>
<p>I'm so happy to hear that Xavier is working on verification of Rust programs on the basis of RustHorn!</p>



<a name="201684772"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/183875-wg-formal-methods/topic/RustHorn/near/201684772" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> Yusuke Matsushita <a href="https://rust-lang.github.io/zulip_archive/stream/183875-wg-formal-methods/topic/RustHorn.html#201684772">(Jun 23 2020 at 03:31)</a>:</h4>
<p>I found the method of RustHorn itself after about a month of thinking about Rust's type system, but it took a fairly long time to understand it better and find the correctness proof for it. I didn't even notice the notion of prophecy variables until reviewers of the paper told me about that.</p>



<a name="201685027"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/183875-wg-formal-methods/topic/RustHorn/near/201685027" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> Yusuke Matsushita <a href="https://rust-lang.github.io/zulip_archive/stream/183875-wg-formal-methods/topic/RustHorn.html#201685027">(Jun 23 2020 at 03:38)</a>:</h4>
<p>I feel that there are still a lot to study in the direction of RustHorn <span aria-label="wink" class="emoji emoji-1f609" role="img" title="wink">:wink:</span></p>



<a name="201723729"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/183875-wg-formal-methods/topic/RustHorn/near/201723729" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> Xavier Denis <a href="https://rust-lang.github.io/zulip_archive/stream/183875-wg-formal-methods/topic/RustHorn.html#201723729">(Jun 23 2020 at 13:18)</a>:</h4>
<p><span class="user-mention" data-user-id="221527">@Yusuke Matsushita</span> , you're going to be working at MPI soon, right?</p>



<a name="201725653"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/183875-wg-formal-methods/topic/RustHorn/near/201725653" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> Yusuke Matsushita <a href="https://rust-lang.github.io/zulip_archive/stream/183875-wg-formal-methods/topic/RustHorn.html#201725653">(Jun 23 2020 at 13:33)</a>:</h4>
<p><span class="user-mention" data-user-id="312719">@Xavier Denis</span> Yes, I'll do an internship at MPI's RustBelt team from September! (Maybe virtually, with 7 hours' time-zone difference from Japan.)</p>



<a name="201727551"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/183875-wg-formal-methods/topic/RustHorn/near/201727551" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> Xavier Denis <a href="https://rust-lang.github.io/zulip_archive/stream/183875-wg-formal-methods/topic/RustHorn.html#201727551">(Jun 23 2020 at 13:47)</a>:</h4>
<p>rough! hopefully you can make it to europe :)</p>



<a name="201729191"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/183875-wg-formal-methods/topic/RustHorn/near/201729191" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> Yusuke Matsushita <a href="https://rust-lang.github.io/zulip_archive/stream/183875-wg-formal-methods/topic/RustHorn.html#201729191">(Jun 23 2020 at 13:59)</a>:</h4>
<p><span class="user-mention" data-user-id="312719">@Xavier Denis</span> Thank you <span aria-label="smiley" class="emoji emoji-1f603" role="img" title="smiley">:smiley:</span></p>



<hr><p>Last updated: Aug 07 2021 at 22:04 UTC</p>
</html>